• A tool for the convergence of multilevel modelling approaches 

      Macías, Fernando; Rutle, Adrian; Stolz, Volker (Journal article; Peer reviewed, 2018)
      Multilevel Modelling is a powerful paradigm that can improve the way we create and use models. The community and approaches related to Multilevel Modelling have been constantly growing, and the need to agree on some basic ...
    • Adaptive distributed monitors of spatial properties for cyber–physical systems 

      Audrito, Giorgio; Casadei, Roberto; Damiani, Ferruccio; Stolz, Volker; Viroli, Mirko (Peer reviewed; Journal article, 2021)
      Cyber–physical systems increasingly feature highly-distributed and mobile deployments of devices spread over large physical environments: in these contexts, it is generally very difficult to engineer trustworthy critical ...
    • An Approach to Flexible Multilevel Modelling 

      Macias, Fernando; Rutle, Adrian; Stolz, Volker; Rodriguez-Echeverria, Roberto; Wolter, Uwe Egbert (Journal article; Peer reviewed, 2018)
      Multilevel modelling approaches tackle issues related to lack of flexibility and mixed levels of abstraction by providing features like deep modelling and linguistic extension. However, the lack of a clear consensus on ...
    • Application of Model-based Testing on a Quorum-based Distributed Storage 

      Wang, Rui; Kristensen, Lars Michael; Meling, Hein; Stolz, Volker (Peer reviewed; Journal article, 2017)
    • Automated test case generation for the Paxos single-decree protocol using a Coloured Petri Net model 

      Wang, Rui; Kristensen, Lars Michael; Meling, Hein; Stolz, Volker (Peer reviewed; Journal article, 2019)
      Implementing test suites for distributed software systems is a complex and time-consuming task due to the number of test cases that need to be considered in order to obtain high coverage. We show how a formal Coloured Petri ...
    • Coverage visualization and analysis of net inscriptions in coloured Petri net models 

      Ahishakiye, Faustin; Requeno Jarabo, Jose Ignacio; Kristensen, Lars Michael; Stolz, Volker (Peer reviewed; Journal article, 2023)
      High-level Petri nets such as coloured Petri nets (CPNs) are characterized by the combination of Petri nets and a high-level programming language. In CPNs and CPN Tools, the inscriptions (e.g. arc expressions and guards) ...
    • Distributed runtime verification by past-CTL and the field calculus 

      Audrito, Giorgio; Damiani, Ferruccio; Stolz, Volker; Torta, Gianluca; Viroli, Mirko (Peer reviewed; Journal article, 2022)
      Recent trends in the engineering of software-intensive systems increasingly promote the adoption of computation at the edge of the network, in the proximity of where sensing and actuation are performed. Applications are ...
    • Enforced Dependencies for Active Objects 

      Pun, Violet Ka I; Stolz, Volker (Peer reviewed; Journal article, 2024)
      We present an active object-based language that records required and provided method completions ahead of method invocations. With this language, a programmer can use method declarations to specify the dependencies between ...
    • Hardware-Assisted Online Data Race Detection 

      Ahishakiye, Faustin; Requeno Jarabo, Jose Ignacio; Pun, Ka I; Stolz, Volker (Chapter; Peer reviewed, 2021)
      Dynamic data race detection techniques usually involve invasive instrumentation that makes it impossible to deploy an executable with such checking in the field, hence making errors difficult to debug and reproduce. This ...
    • I Can See Clearly Now: Clairvoyant Assertions for Deadlock Checking 

      Abusdal, Ole Jørgen; Din, Crystal Chang; Pun, Violet Ka I; Stolz, Volker (Peer reviewed; Journal article, 2022)
      Static analysers are traditionally used to check various correctness properties of software. In the face of refactorings that can have adverse effects on correctness, developers need to analyse the code after refactoring ...
    • MBT/CPN: A Tool for Model-Based Software Testing of Distributed Systems Protocols Using Coloured Petri Nets 

      Wang, Rui; Kristensen, Lars Michael; Stolz, Volker (Peer reviewed; Journal article, 2018)
      Model-based testing is an approach to software testing based on generating test cases from models. The test cases are then executed against a system under test. Coloured Petri Nets (CPNs) have been widely used for modeling, ...
    • MC/DC Test Cases Generation Based on BDDs 

      Ahishakiye, Faustin; Requeno Jarabo, Jose Ignacio; Kristensen, Lars Michael; Stolz, Volker (Chapter; Peer reviewed, 2021)
      We present a greedy approach to test-cases selection for single decisions to achieve MC/DC-coverage of their Boolean conditions. Our heuristics take into account “don’t care” inputs through three-valued truth values that ...
    • Methods and Tool Support for Refinement, Model Transformation and Verification of Network Systems 

      Liu, Zhiming; Stolz, Volker (Others, 2019)
      This compendium contains the lecture notes used in the “BeChong” meetings held as part of the SIU-funded bilateral project “Methods and Tool Support for Re nement, Model Transformation and Veri cation of Network Systems” ...
    • Model-based software testing for distributed systems and protocols 

      Wang, Rui (Doctoral thesis, 2020)
      Society is increasingly dependent on fault-tolerant cloud-based services which rely on the correctness and reliability of advanced distributed software systems and consensus protocols. The implementations of these systems ...
    • MultEcore: Combining the best of fixed-level and multilevel metamodelling 

      Macias Gomez de Villar, Fernando; Rutle, Adrian; Stolz, Volker (Peer reviewed; Journal article, 2016)
      Mainstream metamodelling approaches based on the OMG standards, such as EMF, have a fixed number of modelling levels. Despite their partial acceptance in industry, limitations on the number of levels has led to problems ...
    • Multi-objective Search for Model-based Testing 

      Wang, Rui; Artho, Cyrille; Kristensen, Lars Michael; Stolz, Volker (Chapter; Peer reviewed, 2020)
      This paper presents a search-based approach relying on multi-objective reinforcement learning and optimization for test case generation in model-based software testing. Our approach considers test case generation as an ...
    • On Distributed Runtime Verification by Aggregate Computing 

      Audrito, Giorgio; Damiani, Ferruccio; Stolz, Volker; Viroli, Mirko (Journal article; Peer reviewed, 2019)
      Runtime verification is a computing analysis paradigm based on observing a system at runtime (to check its expected behaviour) by means of monitors generated from formal specifications. Distributed runtime verification is ...
    • Proceedings of the PhD Symposium at iFM’19on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’19) 

      Pun, Ka I; Stolz, Volker; Fazeldehkordi, Elahe; Owe, Olaf; Ramezanifarkhani, Toktam; Damasceno, Carlos Diego Nascimento; Damasceno, Carlos Diego Nascimento; Ahishakiye, Faustin; Kristensen, Lars Michael; Tabar, Asmae Heydari; Bubel, Richard; Hähnle, Reiner; Sagemüller, Justus; Verdier, Olivier (HVL-rapport;14/2020, Report, 2020)
      Preface: This research report contains the proceedings of the PhD Symposium at iFM’19 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM’19), which was held on 3 December, 2019 at Western Norway ...
    • Refactoring and Active Object Languages 

      Stolz, Volker; Pun, Ka I; Gheyi, Rohit (Peer reviewed; Journal article, 2020)
      Refactorings are important for object-oriented (OO) programs. Actor- and active object programs place an emphasis on concurrency. In this article, we show how well-known OO refactorings such as Hide Delegate, Move Method, ...